Termination Proof Script
Consider the TRS R consisting of the rewrite rules
1:
X
*
(Y
+
1
)
→ (X
*
(Y
+
(
1
*
0
)))
+
X
2:
X
*
1
→ X
3:
X
*
0
→ X
4:
X
*
0
→
0
There are 2 dependency pairs:
5:
X
*#
(Y
+
1
)
→ X
*#
(Y
+
(
1
*
0
))
6:
X
*#
(Y
+
1
)
→
1
*#
0
The approximated dependency graph contains one SCC: {5}.
Consider the SCC {5}.
The constraints could not be solved.
Tyrolean Termination Tool
(0.09 seconds) --- May 4, 2006